/******************************************************
Compile : gcc -O3 -o infer infer.c enhance-sim.c utils.c solver.c solver-utils.c -lm
******************************************************/

#include "solver.h"
#include "infer.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <sys/time.h> 

extern solver *solver_copy(solver *);

void print_help ()
{
	printf ("Usage		: ./infer inputfile trigger model\n");
	printf ("		 (./infer input-1 1 3)\n\n");
	printf ("trigger	: 1 first node is a trigger node\n");
	printf ("model		: 0 SIM; 1 SIM + Reliable Trans; 2 SIM + Convergence; 3 SIM + Reliable Trans + Convergence\n\n");
}

/* restriciton of the turnover */
int setup_turnover_numbers (int N, int L, int R[N + 1], int C[N][L - 1][R[N] + 1], int S[L][N], solver *s, int base)
{
	int i, j;

	veci lits;
	veci_new (&lits);
	lit *begin;
	int var;

	int T[L - 2]; /* turnover variable */

	/* restriction of the maximum R[i] turnovers for one nodees */
	for (i = 0; i < N; i++)
	{
		for (j = 0; j < L - 2; j++)
		{
			T[j] = base + j;
		}

		for (j = 0; j < L - 2; j++)
		{
			setup_turnover (S[j][i], S[j + 1][i], T[j], s);
		}

		base = counter_positive1 (L - 2, T, R[i], R[N], C[i], s, base + L - 2);
	}

	veci_delete (&lits);

	return base;
}

/* restriction for order */
int setup_turnover_orders (int N, int L, int MAX_R, int C[N][L - 1][MAX_R + 1], int M, int R2[M][5], solver *s, int base)
{
	int i, j;

	int X[L - 2], Y[L - 2];

	for (i = 0; i < M; i++)
	{
		for (j = 1; j < L - 1; j++)
		{
			X[j - 1] = C[R2[i][0]][j][R2[i][1]];
			Y[j - 1] = C[R2[i][2]][j][R2[i][3]];
		}
		if (R2[i][4] == 0)
			base = check_order2 (L - 2, X, Y, s, base);
		else if (R2[i][4] == 1)
			base = check_order1 (L - 2, X, Y, s, base);
	}

	return base;
}

int do_infer (struct infer *infer, int L)
{
	int i, j, m;
	int N, M, length;

	N = infer->N;

	int pathway[L][N], R1[N + 1];
	int S[L][N]; /* state variable */
	int g[N][N], r[N][N]; /* network variable ; g[i][j]/r[i][j] edge from j to i */

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			S[i][j] = i * N + j;
			pathway[i][j] = -1;
		}
	}

	for (i = 0; i < N; i++)
	{
		for (j = 0; j < N; j++)
		{
			g[i][j] = L * N + i * N + j;
			r[i][j] = L * N + N * N + i * N + j;
		}
	}

	for (i = 0; i < N + 1; i++)
	{
		R1[i] = infer->flips[i];
	}

	for (i = 0; i < N; i++)
	{
		pathway[0][i] = infer->init[i];
	}

	for (i = 0; i < N; i++)
	{
		if (infer->flips[i] % 2 == 0)
			pathway[L - 1][i] = pathway[0][i];
		else
			pathway[L - 1][i] = 1 - pathway[0][i];

		pathway[L - 2][i] = pathway[L - 1][i];
	}

	if (infer->trigger == 1)
	{
		for (i = 1; i < L - 2; i++)
		{
			pathway[i][0] = 0;
		}
	}

	M = infer->M;
	
	int R2[M][5];

	for (i = 0; i < M; i++)
	{
		R2[i][0] = infer->timeorder[i].n1;
		R2[i][1] = infer->timeorder[i].flip1;
		R2[i][2] = infer->timeorder[i].n2;
		R2[i][3] = infer->timeorder[i].flip2;
		R2[i][4] = infer->timeorder[i].type;
	}

	solver *s;
	bool st;

	s = solver_new ();

	m = 2 * N * N + L * N;

	/* restriction of the strong inhibition rules */
	m = sim_model (N, L, pathway, S, g, r, s, m);

	if (infer->model == 1)
	{
		m = reliable_trans (N, infer->trigger, L, S, g, r, s, m);
	}
	else if (infer->model >= 2)
	{
		if (infer->model == 3)
		{
			/* restriction of the quickflips */
			forbidden_quickflips (infer->trigger, N, L, S, s);
		}
		m = convergence (N, infer->trigger, L, S, g, r, s, m);
	}

	/* prevention the early fix point */
	//m = set_fixpoint (N, L, S, s, m);

	/* setup the known values in the pathway */
	set_pathway (N, L, pathway, S, s);

	int C[N][L - 1][R1[N] + 1];

	/* restriction of the number of flips */
	m = setup_turnover_numbers (N, L, R1, C, S, s, m);
	
	/* restriction of the timeorder of flips */
	m = setup_turnover_orders (N, L, R1[N], C, M, R2, s, m);

	st = solver_simplify (s);
	if (st == true)
		st = solver_solve (s,0,0);

	if (st == true)
	{
		for (i = 1; i < L - 2; i++)
		{
			for (j = 0; j < N; j++)
			{
				if (s->model.ptr[S[i][j]] == l_True)
					pathway[i][j] = 1;
				else
					pathway[i][j] = 0;
			}
		}

		for (i = L - 2; i > 0; i--)
		{
			for (j = 0; j < N; j++)
			{
				if (pathway[i][j] != pathway[i - 1][j])
					break;
			}
			if (j != N)
			{
				length = i + 2;
				break;
			}
		}

		printf ("c Candidate Pathway %d\n", length);
		for (i = 0; i < length; i++)
		{
			for (j = 0; j < N; j++)
			{
				printf ("%d ", pathway[i][j]);
			}
			printf ("\n");
		}
	}
	else
	{
		length = 0;
		printf ("No solution!\n");
	}

	solver_delete (s);

	return length;
}

void read_inputfile (int argc, char *argv[], struct infer *infer)
{
	FILE *fp;
	int i, N, L, M;

	infer->trigger = atoi (argv[2]);
	infer->model = atoi (argv[3]);
	fp = fopen (argv[1], "r");
	fscanf (fp, "%d %d", &N, &L);
	infer->N = N;

	infer->init = calloc (sizeof (int), N);
	for (i = 0; i < N; i++)
	{
		fscanf (fp, "%d", &(infer->init[i]));
		if (infer->init[i] != 0 && infer->init[i] != 1)
		{
			printf ("Node's status can only be 1(on) or 0(off)\n");
			exit (0);
		}
	}

	infer->flips = calloc (sizeof (int), N + 1);
	infer->flips[N] = 0;
	infer->maxL = 2;
	for (i = 0; i < N; i++)
	{
		fscanf (fp, "%d", &(infer->flips[i]));
		if (infer->trigger != 1 || i != 0)
			infer->maxL += infer->flips[i];
		if (infer->flips[N] < infer->flips[i])
			infer->flips[N] = infer->flips[i];
	}

	if (infer->trigger == 1)
	{
		if (infer->init[0] == 0 || infer->flips[0] != 1)
		{
			printf ("The first node in the inputfile is not the trigger node.\n");
			exit (0);
		}
	}

	if (infer->model == 0 || infer->model == 2)
	{
		infer->minL = infer->flips[N] + 2;
	}
	else if (infer->model == 1 || infer->model == 3)
	{
		infer->minL = 2 * infer->flips[N] + 1;
	}

	fscanf (fp, "%d", &M);

	infer->M = M;
	infer->timeorder = calloc (sizeof (timeorder), M);

	for (i = 0; i < M; i++)
	{
		fscanf (fp, "%d %d %d %d %d", &(infer->timeorder[i].n1), &(infer->timeorder[i].flip1), &(infer->timeorder[i].n2), &(infer->timeorder[i].flip2), &(infer->timeorder[i].type));
	}

	fclose (fp);
}

int main (int argc, char *argv[])
{
	int i, length;
	struct infer infer;
	struct timeval tpstart,tpend;
	float timeuse;
	gettimeofday(&tpstart,NULL);

	if (argc == 1)
	{
		print_help ();
		exit (0);
	}

	read_inputfile (argc, argv, &infer);

	length = do_infer (&infer, infer.maxL);

	gettimeofday(&tpend,NULL); 
	timeuse = 1000000 * (tpend.tv_sec-tpstart.tv_sec) + tpend.tv_usec-tpstart.tv_usec; 
	timeuse /= 1000000; 

	int flips;

	flips = 0;
	for (i = 0; i < infer.N; i++)
	{
		flips += infer.flips[i];
	}

	printf("Used Time : %8.2f\tNumber of flips : %2d %2d\tNumber of steps : %2d\n", timeuse, flips, infer.flips[infer.N], length);

	/*
	for (i = infer.minL; i <= infer.maxL; i++)
	{
		do_infer (&infer, i);
	}
	*/
}
